Search Results

Documents authored by Draghici, Andrei

Document
DOI: 10.4230/LIPIcs.STACS.2024.29
Semënov Arithmetic, Affine {VASS}, and String Constraints

Authors: Andrei Draghici, Christoph Haase, and Florin Manea

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study extensions of Semënov arithmetic, the first-order theory of the structure ⟨ℕ,+,2^x⟩. It is well-known that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the Büchi V₂-predicate. We therefore restrict ourselves to the existential theory of Semënov arithmetic and show that this theory is decidable in EXPSPACE when extended with arbitrary regular predicates over tuples of number strings. Our approach relies on a reduction to the language emptiness problem for a restricted class of affine vector addition systems with states, which we show decidable in EXPSPACE. As an application of our result, we settle an open problem from the literature and show decidability of a class of string constraints involving length constraints.
Cite as

Andrei Draghici, Christoph Haase, and Florin Manea. Semënov Arithmetic, Affine {VASS}, and String Constraints. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{draghici_et_al:LIPIcs.STACS.2024.29,
  author =	{Draghici, Andrei and Haase, Christoph and Manea, Florin},
  title =	{{Sem\"{e}nov Arithmetic, Affine \{VASS\}, and String Constraints}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.29},
  URN =		{urn:nbn:de:0030-drops-197393},
  doi =		{10.4230/LIPIcs.STACS.2024.29},
  annote =	{Keywords: arithmetic theories, B\"{u}chi arithmetic, exponentiation, vector addition systems with states, string constraints}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact